f2(a, x) -> f2(g1(x), x)
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
↳ QTRS
↳ DependencyPairsProof
f2(a, x) -> f2(g1(x), x)
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
F2(a, x) -> G1(x)
F2(a, x) -> F2(g1(x), x)
G1(h1(x)) -> G1(x)
H1(g1(x)) -> H1(a)
f2(a, x) -> f2(g1(x), x)
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F2(a, x) -> G1(x)
F2(a, x) -> F2(g1(x), x)
G1(h1(x)) -> G1(x)
H1(g1(x)) -> H1(a)
f2(a, x) -> f2(g1(x), x)
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
G1(h1(x)) -> G1(x)
f2(a, x) -> f2(g1(x), x)
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
G1(h1(x)) -> G1(x)
POL( h1(x1) ) = 3x1 + 3
POL( G1(x1) ) = 2x1 + 3
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
f2(a, x) -> f2(g1(x), x)
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
F2(a, x) -> F2(g1(x), x)
f2(a, x) -> f2(g1(x), x)
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F2(a, x) -> F2(g1(x), x)
POL( h1(x1) ) = max{0, -3}
POL( a ) = 1
POL( F2(x1, x2) ) = 2x1 + 2x2 + 3
POL( g1(x1) ) = max{0, -1}
g1(h1(x)) -> g1(x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
f2(a, x) -> f2(g1(x), x)
h1(g1(x)) -> h1(a)
g1(h1(x)) -> g1(x)
h1(h1(x)) -> x